plus(s(s(x)), y) → s(plus(x, s(y)))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(s(0), y) → s(y)
plus(0, y) → y
ack(0, y) → s(y)
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, plus(y, ack(s(x), y)))
↳ QTRS
↳ DependencyPairsProof
plus(s(s(x)), y) → s(plus(x, s(y)))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(s(0), y) → s(y)
plus(0, y) → y
ack(0, y) → s(y)
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, plus(y, ack(s(x), y)))
ACK(s(x), 0) → ACK(x, s(0))
ACK(s(x), s(y)) → ACK(s(x), y)
PLUS(s(s(x)), y) → PLUS(x, s(y))
ACK(s(x), s(y)) → ACK(x, plus(y, ack(s(x), y)))
PLUS(x, s(s(y))) → PLUS(s(x), y)
ACK(s(x), s(y)) → PLUS(y, ack(s(x), y))
plus(s(s(x)), y) → s(plus(x, s(y)))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(s(0), y) → s(y)
plus(0, y) → y
ack(0, y) → s(y)
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, plus(y, ack(s(x), y)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
ACK(s(x), 0) → ACK(x, s(0))
ACK(s(x), s(y)) → ACK(s(x), y)
PLUS(s(s(x)), y) → PLUS(x, s(y))
ACK(s(x), s(y)) → ACK(x, plus(y, ack(s(x), y)))
PLUS(x, s(s(y))) → PLUS(s(x), y)
ACK(s(x), s(y)) → PLUS(y, ack(s(x), y))
plus(s(s(x)), y) → s(plus(x, s(y)))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(s(0), y) → s(y)
plus(0, y) → y
ack(0, y) → s(y)
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, plus(y, ack(s(x), y)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
PLUS(s(s(x)), y) → PLUS(x, s(y))
PLUS(x, s(s(y))) → PLUS(s(x), y)
plus(s(s(x)), y) → s(plus(x, s(y)))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(s(0), y) → s(y)
plus(0, y) → y
ack(0, y) → s(y)
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, plus(y, ack(s(x), y)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(s(s(x)), y) → PLUS(x, s(y))
PLUS(x, s(s(y))) → PLUS(s(x), y)
The value of delta used in the strict ordering is 16.
POL(PLUS(x1, x2)) = (4)x_1 + (4)x_2
POL(s(x1)) = 4 + x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
plus(s(s(x)), y) → s(plus(x, s(y)))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(s(0), y) → s(y)
plus(0, y) → y
ack(0, y) → s(y)
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, plus(y, ack(s(x), y)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
ACK(s(x), 0) → ACK(x, s(0))
ACK(s(x), s(y)) → ACK(s(x), y)
ACK(s(x), s(y)) → ACK(x, plus(y, ack(s(x), y)))
plus(s(s(x)), y) → s(plus(x, s(y)))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(s(0), y) → s(y)
plus(0, y) → y
ack(0, y) → s(y)
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, plus(y, ack(s(x), y)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACK(s(x), 0) → ACK(x, s(0))
ACK(s(x), s(y)) → ACK(x, plus(y, ack(s(x), y)))
Used ordering: Polynomial interpretation [25,35]:
ACK(s(x), s(y)) → ACK(s(x), y)
The value of delta used in the strict ordering is 2.
POL(plus(x1, x2)) = 15/4 + (4)x_2
POL(ACK(x1, x2)) = (1/2)x_1
POL(s(x1)) = 4 + x_1
POL(0) = 0
POL(ack(x1, x2)) = 4 + (4)x_1 + (4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
ACK(s(x), s(y)) → ACK(s(x), y)
plus(s(s(x)), y) → s(plus(x, s(y)))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(s(0), y) → s(y)
plus(0, y) → y
ack(0, y) → s(y)
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, plus(y, ack(s(x), y)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACK(s(x), s(y)) → ACK(s(x), y)
The value of delta used in the strict ordering is 4.
POL(ACK(x1, x2)) = (4)x_2
POL(s(x1)) = 1 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
plus(s(s(x)), y) → s(plus(x, s(y)))
plus(x, s(s(y))) → s(plus(s(x), y))
plus(s(0), y) → s(y)
plus(0, y) → y
ack(0, y) → s(y)
ack(s(x), 0) → ack(x, s(0))
ack(s(x), s(y)) → ack(x, plus(y, ack(s(x), y)))